the_w:World, tg:Id, mss:(Msg List). w-tagged(tg;mss)  (Msg List) 

latex

Definitions	x:A. B(x), Msg, t  T, w-tagged(tg;mss), w.M, t.1, t.2, World
Lemmas	filter wf, Msg wf, eq id wf, mtag wf, Id wf, world wf